package com.googlecode.kipler.satisfiability.completion.branching;

import com.googlecode.kipler.container.dl.DependencySet;

public class Backjumping extends AbstractBacktracking {

	public BranchingPoint apply() {
		DependencySet dependencySet = getException().getDependencySet();
		BranchingPoint currentPoint = getCurrentPoint();
		while (!dependencySet.contains(currentPoint.getWcs())
				&& currentPoint.hasPreviousBranchingPoint()) {
			currentPoint = currentPoint.previousBranchingPoint();
		}
		// we couldn't find the source of clash; it means the initial wcs is
		// unsatisfiable
		if (!dependencySet.contains(currentPoint.getWcs())) {
			currentPoint = new LinearBranchingPoint(null);
		} else {
			currentPoint.getWcs().getData().getLogger().info(
					"Backjumped to WCS " + currentPoint.getWcs().getId());
			currentPoint.setLastBranchDependencies(dependencySet);
		}
		return currentPoint;
	}
}
